The present invention relates generally to tests of logic circuits, and more particularly to a method for analyzing a cause of a non-equivalency that has been found between two logic circuits as a result of verification of equivalency. The present invention is suitable, for example, for a layout design of an IC, such as an LSI.
As electronic apparatuses have recently required to enhance and diversify its functions, ICs, such as LSIs have also required to enhance its functionality. A logic circuit design, such as an LSI layout design, first prepares circuit data called “golden” or “specification”, which has been confirmed to work and achieve given functions through simulations, and then modifies a configuration of a combinational logic circuit by inserting a testing scan circuit, a timing-adjusting buffer circuit, a timing disclosure circuit, etc. into the combinational logic circuit so as to meet various restrictions and conditions about the number of gates, delay timing, etc., without changing functions in the specification. Such data thus obtained by modifying the specification by adding essential elements for actual circuit operations to the specification is called “implementation”. Here, the “combinational logic circuit” is a circuit that includes a combination of basic logic circuit elements (such as AND, OR, EXCLUSIVE OR (“EOR”), and NOT) and determines an output in accordance with one or more input(s). The input is given, for example, from a sequence circuit that holds its own state, such as a counter and a shift register latch. Then, it should be verified whether logic circuits in the specification and implementation are logically equivalent so as to maintain given functions in the specification.
One conceivable equivalency verification method would be to use the logic simulation that checks whether outputs have the same value in response to the same input pattern applied to both the specification and implementation. However, this method cannot guarantee the equivalency until it tries all the input patterns. The verification requires the total number of patterns of 2n where n is the number of circuit inputs from the outside and for reality the simulation cannot try all the patterns for n of several scores.
Accordingly, a conventional method for verifying the logical equivalency between logic circuits in the specification and implementation defines part including all inputs and logic circuit elements that affect one output (referred to as “logic cone” hereinafter) for each combinational logic circuit, and verify the equivalency for each logic cone, for example, after a designer manually pairs logic circuit elements. When both are determined logically non-equivalent, a logical expression of the logic cone causing the non-equivalency is indicated and the designer manually identifies a causal logic circuit using the logical expression.
A preparation of the implementation often associates with a modification of combinational logic circuits in the specification for the reasons including a multistage configuration for small areas, priority of speed, etc. Therefore, the implementation's logic circuits differs from one that simply adds new logic circuit elements to the specification, and often modifies the specification's logic circuits, for example, by changing four stage device configuration into two stages. As a result, a corresponding logic circuit element is not easily identifiable, and the logic circuit that causes non-equivalency is often hard to be identified. In particular, the recent demands for enhanced and diversified LSI functionality have increased the number of logic circuits, and made the circuit configuration complex, whereby the logic circuit that causes non-equivalency has become increasingly hard to be identified. Therefore, the conventional verification of logic equivalency between logic circuits has been inefficient and time-consuming, delaying IC productions.